perm filename TRY.C1[1,JRA] blob
sn#005809 filedate 1972-10-30 generic text, type T, neo UTF8
00100
00200 PRE_OP:A,↑,↓,1,N,j,BIG,LOC,i;
00300 INF_PRED:≤,=;
00400 EQUALITY:=;
00500 VAR:x,y,z,u,v,X,Y,Z;
00550 AXIOM:
00600 ↑(j)≤x ∧ x≤↓(N) ⊃A(x)≤A(↑(x));
00700 1≤x ∧x≤↓(i) ∧ ↓(i)≤N ⊃A(x)≤BIG;
00800 1≤x ∧ x≤j ∧ j ≤↓(N) ⊃A(x)≤A(↑(j));
00900 A(LOC) = BIG;
01000 1≤LOC ∧ LOC ≤j;
01100 ↑(1)≤i;
01200 LOC =j;
01300 ↑(j)≤i;
01400 ↑(1)≤j ∧ j ≤N;
01500
01600 (↑(y)≤x ∧x≤z ⊃ A(x)≤A(↑(x)))∧(y≤z ⊃A(y)≤A(↑(y))) ⊃(y≤u ∧u≤z ⊃A(u)≤A(↑(u)));
01700
01800 x≤y ∨ y≤x;
01900 x≤y ∧ y≤x ⊃ x=y;
02000 x≤y ∧ y≤z ⊃ x≤z;
02100 x≤↑(x);
02200 ¬↑(x)=x;
02300 y≤x ∨ ↑(x)≤y;
02400 x≤x;
02500 THEOREM: j≤x ∧ x ≤↓(N) ⊃ A(x)≤A(↑(x));
02600 ;